IsField(r) == 0  1  |r|  & (u:|r|. u  0  |r|   u | 1 in r) 

latex

---

clarification:

IsField(r) == 0r  1r  |r|  & (u:|r|. u  0r  |r|   u | 1r in r) 

latex

Up	rings 1
Wellformedness Lemmas	field p wf
Definitions	P & Q, x:A. B(x), P  Q, a  b  T , |r|, 0, a | b in r, 1